Вдосконалено темпоральні логіки як засіб формалізації специфікації телекомунікаційних протоколів. Визначено, що на відміну від існуючих засобів формалізації використання темпоральних логік дозволяє вирішити задачу виявлення протиріч у специфікації протоколу. Висвітлено алгебраїчні методи аналізу телекомунікаційних протоколів. Встановлено використання формальних граматик, що дозволяє вирішити задачу перевірки коректності поведінки й оцінки якості розподілу ресурсів телекомунікаційними протоколами. Вперше розроблено метод верифікації телекомунікаційних протоколів, що дозволяє не тільки виділити набір станів, що не задовольняють специфікації, але й на основі побудови контрприкладу визначити необхідний набір змін у реалізації протоколу щодо усунення не відповідності специфікації.

  Скачати повний текст